($\lambda$$A$,$B$,$p$,$z$. $p$.1) $\in$ $A$:Type$\rightarrow$$B$:($A$$\rightarrow$Type)$\rightarrow$($a$:$A$ $\times$ $B$($a$))$\rightarrow$($\downarrow$True)$\rightarrow$$A$